YES 1.409 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  (((/=) :: (Eq b, Eq a) => Either b a  ->  Either b a  ->  Bool) :: (Eq b, Eq a) => Either b a  ->  Either b a  ->  Bool)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  (((/=) :: (Eq b, Eq a) => Either a b  ->  Either a b  ->  Bool) :: (Eq b, Eq a) => Either a b  ->  Either a b  ->  Bool)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  ((/=) :: (Eq b, Eq a) => Either a b  ->  Either a b  ->  Bool)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xv1400), Succ(xv401000)) → new_primPlusNat(xv1400, xv401000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xv30100), Succ(xv40100)) → new_primMulNat(xv30100, Succ(xv40100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xv3000), Succ(xv4000)) → new_primEqNat(xv3000, xv4000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hh, gf, app(ty_[], bbc)) → new_esEs0(xv302, xv402, bbc)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), app(ty_[], eb), ea) → new_esEs0(xv300, xv400, eb)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), fb, app(ty_Maybe, fc)) → new_esEs(xv301, xv401, fc)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), app(ty_Maybe, dh), ea) → new_esEs(xv300, xv400, dh)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_Maybe, ge), gf, gg) → new_esEs(xv300, xv400, ge)
new_esEs1(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, app(ty_Maybe, dh)), ea), de) → new_esEs(xv300, xv400, dh)
new_esEs1(Left(Just(xv300)), Left(Just(xv400)), app(ty_Maybe, app(app(ty_@2, be), bf)), de) → new_esEs2(xv300, xv400, be, bf)
new_esEs(Just(xv300), Just(xv400), app(app(app(ty_@3, bg), bh), ca)) → new_esEs3(xv300, xv400, bg, bh, ca)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), fb, app(app(app(ty_@3, gb), gc), gd)) → new_esEs3(xv301, xv401, gb, gc, gd)
new_esEs1(Left(xv30), Left(xv40), app(app(ty_Either, df), dg), de) → new_esEs1(xv30, xv40, df, dg)
new_esEs(Just(xv300), Just(xv400), app(ty_Maybe, ba)) → new_esEs(xv300, xv400, ba)
new_esEs0(:(xv300, xv301), :(xv400, xv401), app(ty_Maybe, cb)) → new_esEs(xv300, xv400, cb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_Either, ha), hb), gf, gg) → new_esEs1(xv300, xv400, ha, hb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hh, app(ty_Maybe, baa), gg) → new_esEs(xv301, xv401, baa)
new_esEs1(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, hh), app(app(app(ty_@3, bag), bah), bba)), gg), de) → new_esEs3(xv301, xv401, bag, bah, bba)
new_esEs1(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, hh), gf), app(app(ty_@2, bbf), bbg)), de) → new_esEs2(xv302, xv402, bbf, bbg)
new_esEs1(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], dd), de) → new_esEs0(xv301, xv401, dd)
new_esEs1(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(app(ty_@2, hc), hd)), gf), gg), de) → new_esEs2(xv300, xv400, hc, hd)
new_esEs1(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, app(app(ty_@2, ee), ef)), ea), de) → new_esEs2(xv300, xv400, ee, ef)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hh, app(app(ty_Either, bac), bad), gg) → new_esEs1(xv301, xv401, bac, bad)
new_esEs1(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(app(ty_Either, ha), hb)), gf), gg), de) → new_esEs1(xv300, xv400, ha, hb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_@2, hc), hd), gf, gg) → new_esEs2(xv300, xv400, hc, hd)
new_esEs1(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, app(app(app(ty_@3, eg), eh), fa)), ea), de) → new_esEs3(xv300, xv400, eg, eh, fa)
new_esEs1(Left(Just(xv300)), Left(Just(xv400)), app(ty_Maybe, app(ty_[], bb)), de) → new_esEs0(xv300, xv400, bb)
new_esEs1(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], app(app(app(ty_@3, da), db), dc)), de) → new_esEs3(xv300, xv400, da, db, dc)
new_esEs1(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, hh), app(ty_[], bab)), gg), de) → new_esEs0(xv301, xv401, bab)
new_esEs1(Right(xv30), Right(xv40), bcc, app(ty_Maybe, bcd)) → new_esEs(xv30, xv40, bcd)
new_esEs1(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, hh), gf), app(app(ty_Either, bbd), bbe)), de) → new_esEs1(xv302, xv402, bbd, bbe)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_Either, ec), ed), ea) → new_esEs1(xv300, xv400, ec, ed)
new_esEs1(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, hh), gf), app(ty_[], bbc)), de) → new_esEs0(xv302, xv402, bbc)
new_esEs0(:(xv300, xv301), :(xv400, xv401), dd) → new_esEs0(xv301, xv401, dd)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), app(app(app(ty_@3, eg), eh), fa), ea) → new_esEs3(xv300, xv400, eg, eh, fa)
new_esEs1(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, fb), app(ty_Maybe, fc)), de) → new_esEs(xv301, xv401, fc)
new_esEs(Just(xv300), Just(xv400), app(app(ty_Either, bc), bd)) → new_esEs1(xv300, xv400, bc, bd)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hh, gf, app(app(app(ty_@3, bbh), bca), bcb)) → new_esEs3(xv302, xv402, bbh, bca, bcb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hh, app(ty_[], bab), gg) → new_esEs0(xv301, xv401, bab)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), fb, app(app(ty_@2, fh), ga)) → new_esEs2(xv301, xv401, fh, ga)
new_esEs1(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, fb), app(app(ty_Either, ff), fg)), de) → new_esEs1(xv301, xv401, ff, fg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_[], gh), gf, gg) → new_esEs0(xv300, xv400, gh)
new_esEs1(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(ty_[], gh)), gf), gg), de) → new_esEs0(xv300, xv400, gh)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_@2, ee), ef), ea) → new_esEs2(xv300, xv400, ee, ef)
new_esEs1(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], app(ty_Maybe, cb)), de) → new_esEs(xv300, xv400, cb)
new_esEs1(Left(Just(xv300)), Left(Just(xv400)), app(ty_Maybe, app(app(app(ty_@3, bg), bh), ca)), de) → new_esEs3(xv300, xv400, bg, bh, ca)
new_esEs1(Right(xv30), Right(xv40), bcc, app(ty_[], bce)) → new_esEs0(xv30, xv40, bce)
new_esEs1(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, hh), app(app(ty_Either, bac), bad)), gg), de) → new_esEs1(xv301, xv401, bac, bad)
new_esEs1(Right(xv30), Right(xv40), bcc, app(app(ty_Either, bcf), bcg)) → new_esEs1(xv30, xv40, bcf, bcg)
new_esEs1(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, fb), app(app(app(ty_@3, gb), gc), gd)), de) → new_esEs3(xv301, xv401, gb, gc, gd)
new_esEs1(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, hh), app(app(ty_@2, bae), baf)), gg), de) → new_esEs2(xv301, xv401, bae, baf)
new_esEs1(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, app(ty_[], eb)), ea), de) → new_esEs0(xv300, xv400, eb)
new_esEs(Just(xv300), Just(xv400), app(ty_[], bb)) → new_esEs0(xv300, xv400, bb)
new_esEs1(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(app(app(ty_@3, he), hf), hg)), gf), gg), de) → new_esEs3(xv300, xv400, he, hf, hg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hh, gf, app(ty_Maybe, bbb)) → new_esEs(xv302, xv402, bbb)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), fb, app(app(ty_Either, ff), fg)) → new_esEs1(xv301, xv401, ff, fg)
new_esEs1(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, hh), app(ty_Maybe, baa)), gg), de) → new_esEs(xv301, xv401, baa)
new_esEs1(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(ty_Maybe, ge)), gf), gg), de) → new_esEs(xv300, xv400, ge)
new_esEs1(Left(Just(xv300)), Left(Just(xv400)), app(ty_Maybe, app(ty_Maybe, ba)), de) → new_esEs(xv300, xv400, ba)
new_esEs1(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], app(ty_[], cc)), de) → new_esEs0(xv300, xv400, cc)
new_esEs1(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], app(app(ty_@2, cf), cg)), de) → new_esEs2(xv300, xv400, cf, cg)
new_esEs(Just(xv300), Just(xv400), app(app(ty_@2, be), bf)) → new_esEs2(xv300, xv400, be, bf)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hh, app(app(app(ty_@3, bag), bah), bba), gg) → new_esEs3(xv301, xv401, bag, bah, bba)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hh, gf, app(app(ty_@2, bbf), bbg)) → new_esEs2(xv302, xv402, bbf, bbg)
new_esEs1(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, app(app(ty_Either, ec), ed)), ea), de) → new_esEs1(xv300, xv400, ec, ed)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hh, app(app(ty_@2, bae), baf), gg) → new_esEs2(xv301, xv401, bae, baf)
new_esEs1(Left(Just(xv300)), Left(Just(xv400)), app(ty_Maybe, app(app(ty_Either, bc), bd)), de) → new_esEs1(xv300, xv400, bc, bd)
new_esEs1(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, hh), gf), app(ty_Maybe, bbb)), de) → new_esEs(xv302, xv402, bbb)
new_esEs1(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, fb), app(app(ty_@2, fh), ga)), de) → new_esEs2(xv301, xv401, fh, ga)
new_esEs1(Right(xv30), Right(xv40), bcc, app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs3(xv30, xv40, bdb, bdc, bdd)
new_esEs1(Right(xv30), Right(xv40), bcc, app(app(ty_@2, bch), bda)) → new_esEs2(xv30, xv40, bch, bda)
new_esEs0(:(xv300, xv301), :(xv400, xv401), app(app(app(ty_@3, da), db), dc)) → new_esEs3(xv300, xv400, da, db, dc)
new_esEs1(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], app(app(ty_Either, cd), ce)), de) → new_esEs1(xv300, xv400, cd, ce)
new_esEs0(:(xv300, xv301), :(xv400, xv401), app(app(ty_Either, cd), ce)) → new_esEs1(xv300, xv400, cd, ce)
new_esEs1(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, fb), app(ty_[], fd)), de) → new_esEs0(xv301, xv401, fd)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), fb, app(ty_[], fd)) → new_esEs0(xv301, xv401, fd)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hh, gf, app(app(ty_Either, bbd), bbe)) → new_esEs1(xv302, xv402, bbd, bbe)
new_esEs0(:(xv300, xv301), :(xv400, xv401), app(ty_[], cc)) → new_esEs0(xv300, xv400, cc)
new_esEs1(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, hh), gf), app(app(app(ty_@3, bbh), bca), bcb)), de) → new_esEs3(xv302, xv402, bbh, bca, bcb)
new_esEs0(:(xv300, xv301), :(xv400, xv401), app(app(ty_@2, cf), cg)) → new_esEs2(xv300, xv400, cf, cg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(app(ty_@3, he), hf), hg), gf, gg) → new_esEs3(xv300, xv400, he, hf, hg)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: